Ngôn ngữ lập trình

Ứng dụng thường thấy trong lĩnh vực khoa học máy tính của ngôn ngữ hình thức là Trình biên dịch hay trong các giải thuật về chuỗi (tìm kiếm, hoán vị...).

Một trình biên dịch về cơ bản gồm 2 thành phần riêng biệt. Một là trình phân tích từ vựng (lexical analyser), nó có nhiệm vụ xác định các token của nguồn một chương trình máy tính, ví dụ như các định danh (identifier) (tên của hàm, biến...), các từ khóa (keyword), các ký hiệu... Thành phần thứ 2 là trình phân tích cú pháp (parser) với nhiệm vụ quyết định xem mã nguồn chương trình đó có được viết đúng cú pháp của ngôn ngữ lập trình mà trình biên dịch đó hỗ trợ không. Kết quả của một parser là cây cú pháp trừu tượng (abstract syntax tree) và nó được sử dụng cho các giai đoạn sau của quá trình biên dịch. Hai thành phần đó đều hoạt động dựa trên ngôn ngữ hình thức.

Lý thuyết và hệ thống và dẫn xuất về hình thức

Trong toán logic, một lý thuyết hình thức (formal theory) là một tập các câu (sentence) được biểu diễn trên một ngôn ngữ hình thức.

Một hệ thống hình thức (hay còn gọi là giải tích logic (logical calculus) hay hệ thống logic (logical system) là sự kết hợp của một ngôn ngữ hình thức và một bộ máy suy diễn (deductive apparatus).

Một dẫn xuất (derivation) là một chuỗi hữu hạn các công thức đúng cú pháp.